With the rapid development of science and technology and the continuous improvement of industrial demand, the complexity of various software and hardware designs is also increasing day by day, and the requirements for reliability and safety are continuously increasing. The reliability, safety, and correctness of the system have drawn wide attention from the scientific and industrial fields. Formal verification and testing are the main solutions to this problem. Formal verification methods began with Floyd, Hoare, and Manna's research in program specification and verification in the late 1960s. Model Checking proposed in the early 1980s belongs to a model-based formal verification method. It has a relatively simple idea and a high degree of automation and can be widely used in the verification of hardware circuit systems and network protocol systems. Model checking works as the following: making the system as a finite state transition system, using tense logic to describe verification specification, performing an exhaustive search on the finite state transition system to determine whether the specification is satisfied, and if not, giving counterexamples indicating why unsatisfied. Model checking faces the problem of state space explosion. The so-called state explosion problem means that the number of the system states increases exponentially with the increase of system scale. So researchers in this field use various methods to reduce the searching state space, and the Counterexample-Guided Abstraction Model Checking is a commonly used technique. Counterexample-Guided Abstraction Refinement (CEGAR) technique is based on the following: firstly, generating an abstract model by an abstract method when giving a model and its properties. Abstract models may contain more behavior than the original model, however, the structure and description of the abstract model is simpler than the original model, so it can alleviate state-space explosion problems. Secondly, invoking the model checker to check the formula's validity in the abstract model. If valid, the procedure is terminated; otherwise, giving a counterexample. Thirdly, reconstruction, that is, if a path in the original model corresponding to the counterexample path is successfully found, the procedure ends; otherwise, the counterexample path is a spurious one, when the next iteration process begins, an abstract model is regenerated and verified. Repeat this process until the return is valid or invalid, or the program stops caused by the state space explosion. Dynamic Symbolic Execution Technology is a test combining symbolic execution with concrete execution. Symbolic execution refers to representing the value of a program variable by a symbolic value on the premise of not executing the program, and then simulates program execution to perform the correlation analysis. First, build a Control Flow Graph (CFG) for the program to be analyzed, which is an abstract data structure inside a compiler that uses a digraph to represent a procedural process. In the CFG, simulation execution starts from the entry node. When reaching the branch nodes, the constraint solver can be used to determine which branch is feasible, and all the paths can be explored according to the pre-designed path scheduling strategy. Finally, the analysis result of each path is outputted. Dynamic Symbolic Execution takes a specific numeric value as input, starts the code simulation executor, and gathers all the symbolic constraints from the predicates of the branch statements in the current path. Then a new feasible path constraint is constructed by negating one branch of constraints, and a new feasible specific input is obtained by the constraint solver. Finally, the symbol execution engine performs a new round of analysis on the new input. By using the method generating new input through inputting iteratively, in theory, all possible paths can be calculated and analyzed. The main bottleneck of Dynamic Symbolic Execution Techniques is the path explosion problem, that is, as the number of branches in the program increases, the path increases exponentially. Interpolation is an effective method to alleviate the problem. It is substantially an idea of searching and pruning the branches, which marks feasible nodes for interpolation by using an infeasible path. Interpolation means the constraint that does not reach error locations. For a branch node, if each branch of the node is explored, the interpolant at the node is denoted as a full interpolant, otherwise denoted as a half interpolant. In Dynamic Symbolic Execution, if the path constraints from the start node to the current node satisfy the full interpolants of the current node, the path can be subsumed. That is, it cannot be explored, thus the path explosion problem can be effectively alleviated. For large-scale systems, the abstract model is refined repeatedly when it is verified and the more refinements, the more time it takes. Therefore, it's an urgent problem to find an effective method that can accelerate the verification of abstract model and verify a large-scale program.
In summary, the problem existing in the prior art is that for a large-scale system, the abstract model has too many refinements during verification, and the bottleneck of model checking is the state explosion, which consumes a large amount of memory and time and causes the verification crashes.